Nuprl Lemma : not_over_exists
13,42
postcript
pdf
T
:Type,
Q
:(
T
). (
(
x
:
T
.
Q
(
x
)))
(
x
:
T
.
Q
(
x
))
latex
Up
core
2
,
core
2
Definitions
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
A
,
False
Lemmas
not
wf
origin
T:Type, Q:(T
). (
(
x:T. Q(x))) 
(x:T. Q(x)) T:Type, Q:(T). ((x:T. Q(x))) (x:T. Q(x)) 
T Q Qx:A. B(x) Qx:A. B(x)A